tg:Id, k:Knd, l:IdLnk, T, B:Type, f:(B(T List)).
(rcv(l,tg) = k  T = B)
 @source(l): ma-single-sends0(B;T;k;l;tg;f)  Dsys
 & (D:Dsys.
 & (@source(l): ma-single-sends0(B;T;k;l;tg;f)  D
 & ( D 
 & ( realizes es.
 & ( (e:E. loc(e) = source(l)  Id  kind(e) = k  Knd  valtype(e)  B)
 & ( & (e:E. kind(e) = rcv(l,tg)  Knd  valtype(e)  T)
 & ( & (e:E.
 & ( & (loc(e) = source(l)  Id
 & ( & ( kind(e) = k  Knd
 & ( & ( (L:{e':E| kind(e') = rcv(l,tg)  Knd } List.
 & ( & ( ((e':E. (e'  L)  kind(e') = rcv(l,tg)  Knd & sender(e') = e  E)
 & ( & ( (& (e1, e2:E. e1 before e2  L  (e1 <loc e2))
 & ( & ( (& map(e'.val(e');L) = f(val(e))  T List))) 

latex

Definitions

x:A. B(x), P  Q, t  T, ma-single-sends0(B;T;a;l;tg;f), x. t(x), Prop, S  T, Valtype(da;k), Top, if b t else f fi, true, false, A & B, D realizes es. P(es), P & Q, T, True, rcv(l,tg), b, isrcv(e), isrcv(k), SQType(T), {T}, isl(x), lnk(e), lnk(k), 1of(t), outl(x), b, xL. P(x), AB, A, False, {i..j}, i  j < k, x:A. B(x), P  Q, P  Q, f o g, 2of(t), x(s), , Unit, map(f;as), tagged-list-messages(s;v;L), concat(ll), reduce(f;k;as), Y, (x  l), , , f(x)?z, x  dom(f), deq-member(eq;x;L), , a = b

Lemmas

s-sends-rule, lsrc wf, fpf-empty wf, Id wf, fpf-join wf, Knd wf, fpf-single wf, Kind-deq wf, rcv wf, IdLnk wf, fpf-cap wf, ma-valtype wf, fpf-join-cap-sq, top wf, fpf-cap-single1, fpf-dom wf, bool wf, eqtt to assert, subtype rel self, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, fpf-single-dom, possible-world wf, fair-fifo wf, world wf, d-sub wf, dsys wf, subtype rel wf, squash wf, true wf, es-valtype wf, es-kind wf, w-es wf, es-loc wf, es-E wf, Knd sq, fpf-cap-single, fpf-single-dom-sq, eq knd wf, btrue wf, assert-eq-knd, es-rcv-kind, l member wf, es-isrcv wf, es-lnk wf, es-val wf, append nil sq, map wf, select wf, le wf, length wf1, length-map, select-map, non neg length, pi2 wf, pi1 wf, es-tag wf, event system wf, list-set-type2, es-sender wf, es-kind-rcv, map-map, subtype rel list, map-id, member map, eqof eq btrue, Id sq